Nuprl Definition : gcd_p
11,40
postcript
pdf
gcd_p(
a
;
b
;
y
)
== divides(
y
;
a
)
divides(
y
;
b
)
(
z
:
. (divides(
z
;
a
)
divides(
z
;
b
))
divides(
z
;
y
))
latex
Definitions
x
:
A
.
B
(
x
)
,
,
P
Q
,
P
Q
,
divides(
b
;
a
)
FDL editor aliases
gcd_p
origin
divides(y; b) (
z:
. (divides(z; a) divides(z; b)) 
divides(z; y)) divides(y; b) (z:. (divides(z; a) divides(z; b)) divides(z; y)) x:A. B(x) Q Q